Inference at * 
Iof proof for Lemma inconsistent-bool-eq3:


  b:. (b = (b))  False 

latex

 by ((((D (0)) 
CollapseTHENA (Auto))) 
CCollapseTHEN (AutoBoolCase b)) 

latex

CC1: 

CC1: 1. b : 
CC1: 2. b
CC1:   (tt = ff)  False
CC2: 

CC2: 1. b : 
CC2: 2. (b)
CC2:   (ff = tt)  False
CC.

Definitions	left + right, Unit, , p q, p  q, p  q, a < b, x f y, f(a), a < b, null(as), x =a y, (i = j), i z j, i <z j, p =b q, b, Type, x:A. B(x), b, P  Q, P & Q, x:A  B(x), P  Q, P  Q, x:AB(x), Void, , ff, tt, t  T, s = t, A, , False
Lemmas	iff wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, bool wf, bfalse wf, btrue wf, false wf